Termination w.r.t. Q proof of /tmp/tmpPbxf1t/Ex3_3_25_Bor03

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
PREFIX(L) → NIL
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__nil) → NIL
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__prefix(X)) → PREFIX(activate(X))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → FROM(activate(X))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
PREFIX(L) → NIL
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__nil) → NIL
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__prefix(X)) → PREFIX(activate(X))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → FROM(activate(X))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__app(X1, X2)) → APP(activate(X1), activate(X2)) at position [0] we obtained the following new rules:

ACTIVATE(n__app(n__nil, y1)) → APP(nil, activate(y1))
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__nil, y1)) → APP(nil, activate(y1))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2))
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(X1, X2)) → ZWADR(activate(X1), activate(X2)) at position [0] we obtained the following new rules:

ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__nil, y1)) → APP(nil, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__app(n__nil, y1)) → APP(nil, activate(y1)) at position [0] we obtained the following new rules:

ACTIVATE(n__app(n__nil, y0)) → APP(n__nil, activate(y0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(n__nil, y0)) → APP(n__nil, activate(y0))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(x0, y1)) → ZWADR(x0, activate(y1)) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__zWadr(x0, x1), y1)) → ZWADR(zWadr(activate(x0), activate(x1)), activate(y1)) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__nil, y1)) → ZWADR(nil, activate(y1)) at position [0] we obtained the following new rules:

ACTIVATE(n__zWadr(n__nil, y0)) → ZWADR(n__nil, activate(y0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(n__nil, y0)) → ZWADR(n__nil, activate(y0))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__app(x0, x1), y1)) → ZWADR(app(activate(x0), activate(x1)), activate(y1)) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__from(x0), y1)) → ZWADR(from(activate(x0)), activate(y1)) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__s(x0), y1)) → ZWADR(s(activate(x0)), activate(y1)) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__prefix(x0), y1)) → ZWADR(prefix(activate(x0)), activate(y1)) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil)
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, nil) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, n__nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__nil)) → ZWADR(y0, n__nil)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), nil) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), n__nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__nil)) → ZWADR(zWadr(activate(y0), activate(y1)), n__nil)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), nil) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), n__nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__nil)) → ZWADR(app(activate(y0), activate(y1)), n__nil)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil)
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), nil) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), n__nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

                                                                                    ↳ QDP

                                                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), n__nil)) → ZWADR(from(activate(y0)), n__nil)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

                                                                                    ↳ QDP

                                                                                      ↳ DependencyGraphProof

                                                                                        ↳ QDP

                                                                                          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil)
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), nil) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), n__nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

                                                                                    ↳ QDP

                                                                                      ↳ DependencyGraphProof

                                                                                        ↳ QDP

                                                                                          ↳ Narrowing

                                                                                            ↳ QDP

                                                                                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__s(y0), n__nil)) → ZWADR(s(activate(y0)), n__nil)
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

                                                                                    ↳ QDP

                                                                                      ↳ DependencyGraphProof

                                                                                        ↳ QDP

                                                                                          ↳ Narrowing

                                                                                            ↳ QDP

                                                                                              ↳ DependencyGraphProof

                                                                                                ↳ QDP

                                                                                                  ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil)
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), nil) at position [1] we obtained the following new rules:

ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), n__nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

                                                                                    ↳ QDP

                                                                                      ↳ DependencyGraphProof

                                                                                        ↳ QDP

                                                                                          ↳ Narrowing

                                                                                            ↳ QDP

                                                                                              ↳ DependencyGraphProof

                                                                                                ↳ QDP

                                                                                                  ↳ Narrowing

                                                                                                    ↳ QDP

                                                                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__nil)) → ZWADR(prefix(activate(y0)), n__nil)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Narrowing

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ QDP

                                          ↳ Narrowing

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ Narrowing

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ Narrowing

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ QDP

                                                                  ↳ Narrowing

                                                                    ↳ QDP

                                                                      ↳ DependencyGraphProof

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ DependencyGraphProof

                                                                                ↳ QDP

                                                                                  ↳ Narrowing

                                                                                    ↳ QDP

                                                                                      ↳ DependencyGraphProof

                                                                                        ↳ QDP

                                                                                          ↳ Narrowing

                                                                                            ↳ QDP

                                                                                              ↳ DependencyGraphProof

                                                                                                ↳ QDP

                                                                                                  ↳ Narrowing

                                                                                                    ↳ QDP

                                                                                                      ↳ DependencyGraphProof

                                                                                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__zWadr(y0, n__app(x0, x1))) → ZWADR(y0, app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__s(x0))) → ZWADR(prefix(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__zWadr(x0, x1))) → ZWADR(prefix(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__prefix(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__prefix(x0))) → ZWADR(s(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__prefix(x0))) → ZWADR(prefix(activate(y0)), prefix(activate(x0)))
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(YS)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__app(X1, X2)) → ACTIVATE(X2)
ZWADR(cons(X, XS), cons(Y, YS)) → APP(Y, cons(X, n__nil))
ACTIVATE(n__zWadr(n__from(y0), n__s(x0))) → ZWADR(from(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__from(x0))) → ZWADR(s(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__from(x0))) → ZWADR(app(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__app(x0, x1))) → ZWADR(from(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__s(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__zWadr(x0, x1))) → ZWADR(s(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), x0)) → ZWADR(prefix(activate(y0)), x0)
ACTIVATE(n__zWadr(n__s(y0), n__s(x0))) → ZWADR(s(activate(y0)), s(activate(x0)))
ACTIVATE(n__zWadr(y0, n__from(x0))) → ZWADR(y0, from(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__prefix(x0))) → ZWADR(app(activate(y0), activate(y1)), prefix(activate(x0)))
ACTIVATE(n__zWadr(n__prefix(y0), n__app(x0, x1))) → ZWADR(prefix(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), x0)) → ZWADR(zWadr(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(n__app(y0, y1), n__s(x0))) → ZWADR(app(activate(y0), activate(y1)), s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), n__app(x0, x1))) → ZWADR(s(activate(y0)), app(activate(x0), activate(x1)))
ACTIVATE(n__app(x0, y1)) → APP(x0, activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__app(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__app(y0, y1), n__zWadr(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__app(n__from(x0), y1)) → APP(from(activate(x0)), activate(y1))
ACTIVATE(n__prefix(X)) → ACTIVATE(X)
APP(cons(X, XS), YS) → ACTIVATE(XS)
ACTIVATE(n__app(n__zWadr(x0, x1), y1)) → APP(zWadr(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__app(n__app(x0, x1), y1)) → APP(app(activate(x0), activate(x1)), activate(y1))
ACTIVATE(n__zWadr(y0, n__prefix(x0))) → ZWADR(y0, prefix(activate(x0)))
ACTIVATE(n__zWadr(n__app(y0, y1), x0)) → ZWADR(app(activate(y0), activate(y1)), x0)
ACTIVATE(n__zWadr(y0, x0)) → ZWADR(y0, x0)
ACTIVATE(n__app(n__prefix(x0), y1)) → APP(prefix(activate(x0)), activate(y1))
ACTIVATE(n__app(n__s(x0), y1)) → APP(s(activate(x0)), activate(y1))
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__zWadr(x0, x1))) → ZWADR(zWadr(activate(y0), activate(y1)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__zWadr(n__app(y0, y1), n__app(x0, x1))) → ZWADR(app(activate(y0), activate(y1)), app(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__prefix(y0), n__from(x0))) → ZWADR(prefix(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__prefix(x0))) → ZWADR(from(activate(y0)), prefix(activate(x0)))
ACTIVATE(n__zWadr(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__zWadr(n__zWadr(y0, y1), n__from(x0))) → ZWADR(zWadr(activate(y0), activate(y1)), from(activate(x0)))
ACTIVATE(n__zWadr(n__from(y0), n__zWadr(x0, x1))) → ZWADR(from(activate(y0)), zWadr(activate(x0), activate(x1)))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ZWADR(cons(X, XS), cons(Y, YS)) → ACTIVATE(XS)
ACTIVATE(n__zWadr(y0, n__zWadr(x0, x1))) → ZWADR(y0, zWadr(activate(x0), activate(x1)))
ACTIVATE(n__zWadr(n__from(y0), n__from(x0))) → ZWADR(from(activate(y0)), from(activate(x0)))
ACTIVATE(n__zWadr(y0, n__s(x0))) → ZWADR(y0, s(activate(x0)))
ACTIVATE(n__zWadr(n__s(y0), x0)) → ZWADR(s(activate(y0)), x0)
ACTIVATE(n__zWadr(n__from(y0), x0)) → ZWADR(from(activate(y0)), x0)

The TRS R consists of the following rules:

app(nil, YS) → YS
app(cons(X, XS), YS) → cons(X, n__app(activate(XS), YS))
from(X) → cons(X, n__from(n__s(X)))
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X, XS), cons(Y, YS)) → cons(app(Y, cons(X, n__nil)), n__zWadr(activate(XS), activate(YS)))
prefix(L) → cons(nil, n__zWadr(L, n__prefix(L)))
app(X1, X2) → n__app(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
zWadr(X1, X2) → n__zWadr(X1, X2)
prefix(X) → n__prefix(X)
activate(n__app(X1, X2)) → app(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__zWadr(X1, X2)) → zWadr(activate(X1), activate(X2))
activate(n__prefix(X)) → prefix(activate(X))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.